\section{Verifying the solution}\label{s:local}

We start the section with a key property of algorithm $\phragmms$ as motivation.

\begin{theorem}\label{thm:315guarantee}
If a balanced solution $(A,w)$ observes $\supp_w(A)\geq \max_{c'\in C\setminus A} \score(c')$, then it satisfies a) the PJR property and b) a 3.15-approximation guarantee for the maximin support objective. 
Furthermore, testing all conditions (feasibility, balancedness and the previous inequality) can be done in time $O(|E|)$. 
Finally, the output solution of $\phragmms$ is guaranteed to satisfy these conditions.
\end{theorem}

\begin{proof}
The first statement follows from Lemmas \ref{lem:localopt} and \ref{lem:candidate315}, and the third one from Lemma~\ref{lem:315localoptimality}. 
Feasibility (inequality~\ref{eq:feasible}) can clearly be checked in time $O(|E|)$, as can balancedness by Lemma~\ref{lem:balanced}. 
Finally, if $t:=\supp_w(A)$, the inequality in the statement is equivalent to $t\geq \max_{c'\in C\setminus A} \prescore(c',t)$, which is tested with algorithm $\maxprescore(A,w,t)$ in time $O(|E|)$ by Theorem~\ref{thm:runtimes}.
\end{proof}

%This in turn proves Theorem~\ref{thm:intro2}. 
As we argued in the introduction, the result above is one of the most relevant features of our proposed election rule, and is essential for its implementation over a blockchain network as it enables its adaptation into a verifiable computing scheme. As such, the rule may be executed by off-chain workers, leaving only the linear-time tests mentioned in the previous theorem to be performed on-chain, to ensure the quality of the solution found. 
   
To finish the proof of Theorem~\ref{thm:intro2}, it remains to prove Lemma~\ref{lem:localopt} -- which we do at the end of this section -- and show that the verification process above admits a parallel execution -- which we do next. 
In particular, for a parameter $p$, we consider the distribution of this process over $p$ computing units that execute in sequence, such as $p$ consecutive blocks in a blockchain network. 
We remark however that our description below may be easily adapted to concurrent execution if desired.

\begin{lemma}\label{lem:parallel}
For any integer $p\geq 1$, both the input election instance as well as any solution $(A,w)$ to it can be distributed into $p$ data sets, such that each data set is of size $O(|E|/p + |C|)$. 
Moreover, all the tests mentioned in Theorem~\ref{thm:315guarantee} can be executed by $p$ sequential computing units such that each unit only requires access to one data set and runs in time $O(|E|/p + |C|)$. 
Therefore, for $p$ sufficiently large, each unit can be made to run in time $O(|C|)$.
\end{lemma}

\begin{proof}
Partition the voter set $N=\cup_{i=1}^p N^i$ into $p$ subsets of roughly equal size, and let $G^i$ be the subgraph of the input approval graph $G$ induced by $N^i\cup C$ (corresponding to the ballots of voters in $N^i$). 
Consider $p$ data sets where the $i$-th one stores subgraph $G^i$ along with the list of vote strengths for voters in $N^i$. 
%
Next, we assume that an untrusted party provides a solution $(A,w)$, and we assume that they also provide its corresponding vector $(\supp'_w(c))_{c\in A}$ of member supports, where the prime symbol indicates that these are claimed values to be verified. 
This solution is distributed so that the $i$-th data set stores the full committee $A$, the claimed supports, and the restriction $w^i$ of the edge weight vector $w$ over $G^i$. 
Clearly, each data set is of size $O(|E|/p + |C|)$.

Now consider $p$ computing units running in sequence, where the $i$-th unit has access to the $i$-th data set, and recall that the verification of solution $(A,w)$ consists of four tests: a) feasibility, b) balancedness, c) correctness of the claimed member supports, and d) the inequality $t\geq \max_{c'\in C\setminus A} \prescore(c',t)$, where we define $t:=\supp'_w(A)$. 
To avoid dependencies across these tests, our general strategy is to assume that the claimed supports are correct, except obviously for test c. 
For example, since both feasibility (inequality~\ref{eq:feasible}) and balancedness (properties 2 and 3 of Lemma~\ref{lem:balanced}) are checked on a per-voter basis, the $i$-th unit can perform these checks for its own subset of voters $N^i$, using the claimed supports to check property 3 of Lemma~\ref{lem:balanced}. 

Tests c and d, on the other hand, require the cooperation of all units. 
The $i$-th unit can compute a vector $(\supp_{w^i}(c))_{c\in A}$ of supports relative to the local voters in $N^i$, so it follows by induction that it can also compute the partial sum $\sum_{j\leq i} (\supp_{w^j}(c))_{c\in A}$, and communicate it to the $(i+1)$-st unit. The last unit can then compute the full vector $\sum_{j\leq p} (\supp_{w^j}(c))_{c\in A}=(\supp_{w}(c))_{c\in A}$, and check that it matches the claimed supports. 

Similarly, the $i$-th unit can compute the vector $(\slack(n,t))_{n\in N^i}$ of slacks for $N^i$ (equation~\ref{eq:slack}), and use it to find a vector of parameterized scores relative to the local voters, $(\prescore^i(c',t))_{c'\in C\setminus A}$, where $\prescore^i(c', t):=\sum_{n\in N_{c'}\cap N^i} \slack(n,t)$. 
Again by induction, this unit can also find the partial sum $\sum_{j\leq i} (\prescore^j(c',t))_{c'\in C\setminus A}$, and communicate it to the $(i+1)$-st unit. 
The last unit then retrieves the full vector $\sum_{j\leq p} (\prescore^j(c',t))_{c'\in C\setminus A}=(\prescore(c',t))_{c'\in C\setminus A}$, and verifies that all parameterized scores are bounded by $t$. 
Clearly, each unit has a time and memory complexity of $O(|E|/p + |C|)$.
\end{proof}

Next, we begin our analysis of the PJR property by defining a \emph{parametric version} of it, that measures just how well represented the voters are by a given committee $A$. It is a generalization of the property that turns it from binary to quantitative.

\begin{definition}
For any $t\in\R$, a committee $A\subseteq C$ (of any size) satisfies PJR with parameter $t$ ($t$-PJR for short) if, for any group $N'\subseteq N$ of voters and any integer $0<r\leq |A|$, we have that
\begin{itemize}
\item[a)] if $|\cap_{n\in N'} C_n|\geq r$
\item[b)] and $\sum_{n\in N'} s_n \geq r\cdot t$, 
\item[c)] then $|A\cap (\cup_{n\in N'} C_n)|\geq r$.
\end{itemize}
\end{definition}

In words, if there is a group $N'$ of voters with at least $r$ commonly approved candidates, and enough aggregate vote strength to provide each of these candidates with a support of at least $t$, then this group must be represented by at least $r$ members in committee $A$, though not necessarily commonly approved. 
Notice that the standard version of PJR is equivalent to $\hat{t}$-PJR for $\hat{t}:=\sum_{n\in N} s_n / |A|$, and that if a committee satisfies $t$-PJR then it also satisfies $t'$-PJR for each $t'\geq t$, i.e., the property gets stronger as $t$ decreases. 
This is in contrast to the maximin support objective, which implies a stronger property as it increases.

We remark that the notion of \emph{average satisfaction} introduced in~\cite{sanchez2017proportional} also attempts to quantify the level of proportional representation achieved by a committee. 
Informally speaking, that notion measures the average number of representatives in the committee that each voter in a group has, for any group of voters with sufficiently high aggregate vote strength and cohesiveness. 
In contrast, with parametric PJR we focus on providing sufficient representatives to the group as a whole and not to each individual voter, and we measure the aggregate vote strength required to gain adequate representation.
%Interestingly, the average satisfaction measure is closely linked to the EJR property, and in particular in~\cite{aziz2018complexity} this measure is used to prove that a local search algorithm achieves EJR; 
%similarly, in Appendix~\ref{s:LS} we use parametric PJR to prove that a local search version of $\phragmms$ achieves standard PJR.

Testing whether an arbitrary solution satisfies standard PJR is known to be coNP-complete~\cite{aziz2018complexity}, hence the same remains true for its parametric version.
We provide next a sufficient condition for a committee to satisfy $t$-PJR which is efficiently testable, based on our definitions of parameterized score and score.  

\begin{lemma} \label{lem:locality}
If for a feasible solution $(A,w)$ there is a parameter $t\in\R$ such that $\max_{c'\in C\setminus A} \prescore(c',t)<t$, or equivalently, such that $\max_{c'\in C\setminus A} \score(c') <t$, then committee $A$ satisfies $t$-PJR. 
This condition can be tested in $O(|E|)$ time.
\end{lemma}

\begin{proof} 
We prove the contrapositive of the claim. If $A$ does not satisfy $t$-PJR, there must be a subset $N'\subseteq N$ of voters and an integer $r>0$ that observe properties a) and b) above but fail property c). 
By property a) and the negation of c), set $(\cap_{n\in N'} C_n)\setminus A$ must be non-empty: let $c'$ be a candidate in it. 
We will prove that for any feasible weight vector $w\in \R^E$, it holds that $\prescore(c',t)\geq t$, and consequently $\score(c')\geq t$ by the definition of score. We have
%
\begin{align*} 
\prescore(c',t) &= \sum_{n\in N_{c'}}  \slack(n,t) \\
&\geq \sum_{n\in N'} \slack(n,t) \\
&\geq \sum_{n\in N'} \Big(s_n - t\cdot \sum_{c\in A\cap C_n} \frac{w_{nc}}{\supp_w(c)}\Big)  \\
&= \sum_{n\in N'} s_n - t \cdot \sum_{c\in A\cap (\cup_{n\in N'} C_n)} 
\frac{\sum_{n\in N'\cap N_c} w_{nc}}{\sum_{n\in N_c} w_{nc}} \\ 
& \geq t\cdot r - t\cdot |A\cap (\cup_{n\in N'} C_n)| \\
& \geq t\cdot r - t\cdot (r-1) = t, 
\end{align*}
%
where the first inequality holds as $N'\subseteq N_{c'}$ by our choice of candidate $c'$, the second one holds by definition of slack, the third one holds by property b) and because the fraction on the fourth line is at most $1$ for each candidate $c$, and the last inequality holds by negation of c). 
This proves that $\prescore(c',t) \geq t$. 

For a given solution $(A,w)$ and parameter $t$, one can verify the condition above in time $O(|E|)$ by computing $\maxprescore(A,w,t)$ and comparing the output to $t$; see Theorem~\ref{thm:runtimes}.
\end{proof}

The proof of Lemma~\ref{lem:localopt} now follows as a corollary.

\begin{proof}[Proof of Lemma~\ref{lem:localopt}]
Let $c_{\max}$ be a candidate with highest score $t_{\max}=\score(c_{\max})=\max_{c'\in C\setminus A} \score(c')$. 
If $\supp_w(A)\geq t_{\max}$, it follows from Lemma~\ref{lem:insert} that if we execute $\ins(A,w,c_{\max}, t_{\max})$, we obtain a solution $(A+c_{\max}, w')$ with $\supp_{w'}(A+c_{\max})=t_{\max}$. 
Now, by feasibility of vector $w'$, we have the inequality $\sum_{n\in N} s_n \geq \sum_{c\in A+c_{\max}} \supp_{w'}(c) \geq (k+1)\cdot t_{\max}$, which implies that $t_{\max}\leq \sum_{n\in N} s_n / (k+1) < \sum_{n\in N} s_n / k =: \hat{t}$. 
By Lemma~\ref{lem:locality} above, having $t_{\max} < \hat{t}$ implies that $A$ satisfies $\hat{t}$-PJR, which is standard PJR.
\end{proof}

We end the section with the observation that the inequality in Lemma~\ref{lem:localopt}, namely $\supp_w(A)\geq \max_{c'\in C\setminus A} \score(c')$, corresponds to a notion of local optimality for solution $(A,w)$. 
Indeed, if the inequality did not hold we could improve upon the solution by iteratively swapping the member with least support for the unelected candidate with highest score, resulting in an increase of the least member support and/or a decrease of the highest score among unelected candidates, which by Lemma~\ref{lem:locality} strengthens the level of parametric PJR of the solution. 
Therefore, the fact that $\phragmms$ always returns a locally optimal solution (Lemma~\ref{lem:315localoptimality}) implies standard PJR but can be considered to be a strictly stronger property. 
In Appendix~\ref{s:LS}, we formalize this local search algorithm and use it to prove Theorem~\ref{thm:intro3}.
